(set-logic HO_UF)
(set-info :status sat)
(set-option :fmf-bound true)
(set-option :finite-model-find true)
(declare-sort a 0)
(declare-sort b 0)
(declare-sort o 0)
(declare-sort c 0)
(declare-sort d 0)
(declare-sort t 0)
(declare-sort e 0)
(declare-sort f 0)
(declare-fun p () a)
(declare-fun q (o b) a)
(declare-fun r (d c) a)
(declare-fun g (t b) c)
(declare-fun h (e b) t)
(declare-fun s () e)
(declare-fun i (f b) o)
(declare-fun j (d) f)
(declare-fun k (c d) a)
(declare-fun l (d) f)
(assert (forall ((?m d) (?u b) (?n b)) (= (= (q (i (j ?m) ?u) ?n) p) (= (k (g (h s ?u) ?n) ?m) p))))
(assert (forall ((?m d) (?u b) (?n b)) (= (= (q (i (l ?m) ?u) ?n) p) (= (r ?m (g (h s ?u) ?n)) p))))
(check-sat)
